\subsection{Traducción a Lenguaje Específico}

\begin{frame}{Traducción a Lenguaje Específico}
\tableofcontents[currentsection,currentsubsection]
\end{frame}

\begin{frame}[fragile]{Generación de Fórmulas}
\begin{block}
\LARGE  Fórmulas de las restricciones \pause $ \rightarrow $ Código de resolución de restricciones
\end{block}
\end{frame}


\subsubsection{Traducción}

\begin{frame}{Traducción}
Las fórmulas que representan las restricciones se traducen a un lenguaje de programación con restricciones específico, en nuestro caso \alert{MiniZinc}.
\begin{itemize}
\pause \item Declarar las variables con sus tipos
\pause \item Expresar las restricciones
\pause \item Ejecutar el resolutor
\pause \item Establecer formato de salida
\end{itemize}
\end{frame}

\subsubsection{Código de ejemplo}
\begin{frame}[fragile]{Traducción}
\begin{block}{Declaración de variables}
\begin{verbatim}
var int: notas_dni_0;
var int: notas_dni_1;
var int: notas_nota_0;
var int: notas_nota_1;
\end{verbatim}
\end{block}

\begin{block}{Restricciones}
\begin{verbatim}
constraint 
((((true /\ (true /\ (notas_dni_0 != notas_dni_1))) /\ true) 
/\ (notas_nota_0 >= 5)) \/ 
(((true /\ (true /\ (notas_dni_0 != notas_dni_1))) /\ true)
/\ (notas_nota_1 >= 5)));
\end{verbatim}
\end{block}
\end{frame}

\begin{frame}[fragile]{Traducción}
\begin{block}{Llamada al Resolutor}
\begin{verbatim}
solve satisfy;
\end{verbatim}
\end{block}

\begin{block}{Formato de Salida}
\begin{verbatim}
output 
[" INSERT INTO notas (dni,nota) VALUES
 (", show(notas_dni_0),",", show(notas_nota_0),");
"," INSERT INTO notas (dni,nota) VALUES
 (", show(notas_dni_1),",", show(notas_nota_1),");"]; 
\end{verbatim}
\end{block}
\end{frame}
\subsection{Resolución}
\begin{frame}[fragile]{Resolución de Restricciones}
Una vez se tiene el modelo traducido a código MiniZinc se resuelve
\begin{itemize}
\pause\item Con el resolutor propio de MiniZinc:\\
\cod{minizinc modelo.mzn}
\pause\item o traduciendo a código FlatZinc y resolviendo con cualquier resolutor que lo implemente (G12/CPX, Gecode, ECLiPSE, SICtus Prolog, JaCoP,SCIP)\\
\cod{mzn2fzn modelo.mzn; fz modelo.fzn} Si el resolutor elegido es Gecode
\end{itemize}
\end{frame}